(** val type_check : exp list -> exp -> exp -> bool **)

let rec type_check g a m =
  match type_infer g m with
  | Some a0 -> subtyping_impl g (nf_to_exp a0) a
  | None -> false

(** val type_infer : exp list -> exp -> nf option **)

and type_infer g = function
| A_zero -> Some Nf_nat
| A_succ e -> if type_check g A_nat e then Some Nf_nat else None
| A_natrec (e, e0, e1, e2) ->
  if type_check g A_nat e2
  then (match type_infer (A_nat :: g) e with
        | Some a ->
          (match a with
           | Nf_typ _ ->
             if type_check g (A_sub (e, (A_extend (A_id, A_zero)))) e0
             then if type_check (e :: (A_nat :: g)) (A_sub (e, (A_extend ((A_compose (A_weaken, A_weaken)), (A_succ (A_var
                       (Big_int_Z.succ_big_int Big_int_Z.zero_big_int))))))) e1
                  then Some (nbe_ty_impl g (A_sub (e, (A_extend (A_id, e2)))))
                  else None
             else None
           | _ -> None)
        | None -> None)
  else None
| A_nat -> Some (Nf_typ Big_int_Z.zero_big_int)
| A_typ n -> Some (Nf_typ (Big_int_Z.succ_big_int n))
| A_var n -> (match lookup g n with
              | Some a -> Some (nbe_ty_impl g a)
              | None -> None)
| A_fn (e, e0) ->
  (match type_infer g e with
   | Some a ->
     (match a with
      | Nf_typ _ -> (match type_infer (e :: g) e0 with
                     | Some a0 -> Some (Nf_pi ((nbe_ty_impl g e), a0))
                     | None -> None)
      | _ -> None)
   | None -> None)
| A_app (e, e0) ->
  (match type_infer g e with
   | Some s ->
     (match s with
      | Nf_pi (n, n0) ->
        if type_check g (nf_to_exp n) e0 then Some (nbe_ty_impl g (A_sub ((nf_to_exp n0), (A_extend (A_id, e0))))) else None
      | _ -> None)
   | None -> None)
| A_pi (e, e0) ->
  (match type_infer g e with
   | Some a ->
     (match a with
      | Nf_typ n ->
        (match type_infer (e :: g) e0 with
         | Some a0 -> (match a0 with
                       | Nf_typ n0 -> Some (Nf_typ (max n n0))
                       | _ -> None)
         | None -> None)
      | _ -> None)
   | None -> None)
| A_sub (_, _) -> None

(** val type_check_closed : exp -> exp -> bool **)

let type_check_closed a m =
  match type_infer [] a with
  | Some a0 -> (match a0 with
                | Nf_typ _ -> type_check [] a m
                | _ -> false)
  | None -> false